const fs = require("fs");
const { processTimeDetailInfo } = require('./time_detail');

function readFileAsString(filePath) {
  return new Promise((resolve, reject) => {
    fs.readFile(filePath, "utf8", (err, data) => {
      if (err) {
        if (err.errno === -2) {
          resolve({ data: null });
        }
        reject(err);
        return;
      }
      resolve({ data });
    });
  });
}

const capitalizedOnlyFirst = (word) =>
  word.charAt(0).toUpperCase() + word.slice(1).toLowerCase();

function process_ltlfsyn(data) {
  const match = data.match(/^(Unrealizable|Realizable)/);
  if (match) {
    return {
      result: capitalizedOnlyFirst(
        match[0].match(/Unrealizable|Realizable/)[0]
      ),
    };
  } else {
    return {
      result: "Stopped",
    };
  }
}

function getMatchResFor_Combine01(lines, syn_res)
{
  let matchLogLine = null;
  // console.log(lines);
  // throw new Error("NotImplemented");
  for (let i = lines.length - 1; i >= 0; i--)
  {
    const lineStr = lines[i];
    matchLogLine = lineStr.match(/return Realizable after PreCheck!$/);
    let breakFlag = true;
    let matchRaw_arr = null;
    if (matchRaw_arr = lineStr.match(/return (Realizable|Unrealizable) after PreCheck!$/)) {
      matchLogLine = "PreCheck-" + matchRaw_arr[1]
    }
    else if (matchRaw_arr = lineStr.match(/^PreCheck synthesis return (Realizable|Unrealizable)!$/)) {
      matchLogLine = "PreCheck-" + matchRaw_arr[1]
    }
    else if (matchRaw_arr = lineStr.match(/::Group::	SearchWholeDFA \(sub_af in sysGroup\) return (Realizable|Unrealizable)!/)) {
      matchLogLine = "DFA-" + matchRaw_arr[1]
    }
    else if (matchRaw_arr = lineStr.match(/^::Group::	Finish syft_check_DFA_realizability return (Realizable|Unrealizable)$/)) {
      matchLogLine = "DFA-" + matchRaw_arr[1]
    }
    else if (matchRaw_arr = lineStr.match(/^Finish syft_check_DFA_realizability return (Realizable|Unrealizable)$/)) {
      matchLogLine = "DFA-" + matchRaw_arr[1]
    }
    else if (matchRaw_arr = lineStr.match(/^compositional_synthesis return (Realizable|Unrealizable)!$/)) {
      matchLogLine = "DFA-" + matchRaw_arr[1]
    }
    else if (matchRaw_arr = lineStr.match(/^Backward synthesis return (Realizable|Unrealizable)!$/)) {
      matchLogLine = "DFA-" + matchRaw_arr[1]
    }
    else if (matchRaw_arr = lineStr.match(/^SearchWholeDFA return (Realizable|Unrealizable)!$/)) {
      matchLogLine = "DFA-" + matchRaw_arr[1]
    }
    else {
      breakFlag = false;
    }
    if (breakFlag)
        break;
  }
  if (!matchLogLine)
    {
      return "NoLog-" + syn_res;
    }
  if (matchLogLine.substring(matchLogLine.length-syn_res.length) != syn_res)
    {
      console.log(matchLogLine, syn_res);
    return "ERROR";
    }
  return matchLogLine;
}

function process_ltlfsynSyft(data) {
  let match = null;
  const lines = data.split('\n');
  // for (let i = 0; i < lines.length; i++)
  let timout_exited_line_idx = null;
  // console.log('process_ltlfsynSyft', lines.length);
  for (let i = lines.length - 25; i >= 0; i--)
  {
    const lineStr = lines[i];
    // console.log('lineStr', lineStr);
    match = lineStr.match(/^(Unrealizable|Realizable)$/);
    if (match) {
      // console.log(lineStr);
      break;
    }
    if (timout_exited_line_idx != null)
        break;
    if (lineStr.match(/^(Command exited with non-zero status)/)) {
      timout_exited_line_idx = i;
    }
  }
  // console.log('process_ltlfsynSyft', match);
  if (match) {
    const syn_res = match[0].match(/Unrealizable|Realizable/)[0];
    return {
      result: capitalizedOnlyFirst(
        syn_res
      ),
    };
  } else {
    return {
      result: "Stopped",
    };
  }
}

function process_ltlfsynSyft_Cases(data) {
  const lines = data.split('\n');
  if (lines[0].startsWith("+ /usr/bin/time"))
    lines.splice(0, 1);
  const timeoutLines = lines.slice(lines.length - 24);
  const reducedLines = lines.slice(0, lines.length - 24);
  const syn_res_str = reducedLines[reducedLines.length - 1];
  const match = syn_res_str.match(/^(Unrealizable|Realizable)/);
  if (match) {
    return {
      result: capitalizedOnlyFirst(
        getMatchResFor_Combine01(reducedLines, match[0])
      ),
    };
  } else {
    return {
      result: "Stopped",
    };
  }
}

function process_ltlfsynSyft_Details(data) {
  let match = null;
  const lines = data.split('\n');
  if (lines[0].startsWith("+ /usr/bin/time"))
    lines.splice(0, 1);
  let timeoutLines = lines.slice(lines.length - 24);
  let reducedLines = lines.slice(0, lines.length - 24);

  const sub_af_lines = [];
  const group_sub_af_lines = [];
  const syft_lines = [];

  let tmp_match = null;
  for (let i = 0; i < reducedLines.length; i++)
  {
      const line = reducedLines[i];
      if (line.match(/^(dfaMin|dfaAnd)/))
          continue;
      else if (line.match('/^Total CPU time used in synthesis'))
          continue;
      else if (line.match('/^cur_dfa_sz:'))
          syft_lines.append(line);
      else if (line.match('/^::Group::	sub_af:/'))
      {
          group_sub_af_lines.append(line);
          sub_af_lines = [];
      }
      else if (line.match('/^sub_af:/'))
          sub_af_lines.append(line);
      else if (tmp_match = line.match('/^::Group::	split_sys group_num is (\d+)'))
          split_group_num = tmp_match[1];
  }
  const last_group_sub_af = group_sub_af_lines[group_sub_af_lines.length - 1].slice(20);
  const last_sub_af = sub_af_lines[sub_af_lines.length - 1].slice(7);
  reducedLines.filter((line) => {
    if (line.match('/^(dfaMin|dfaAnd)'))
        return false;
    if (line.match('/^Total CPU time used in synthesis'))
        return false;
    if (line.match('/^cur_dfa_sz:'))
      return false;
    return true;
  })

  // console.log(timeoutLines);
  // console.log(reducedLines);

  // console.log("syn_res:\t", reducedLines.pop())
  // console.log(processTimeDetailInfo(timeoutLines.join('\n')));
  const state_cnt_lines = reducedLines.slice(Math.max(0, reducedLines.length - 5)).reverse();
  let state_cnt_match = null;
  for (let i = 0; i < state_cnt_lines.length; i++)
  {
    const lineStr = state_cnt_lines[i];
    state_cnt_match = lineStr.match(/syn_states::get_state_cnt: (-?\d+)/);
    // console.log(lineStr);
    if (state_cnt_match)
    {
      // console.log(state_cnt_match);
      state_cnt_match = state_cnt_match[1];
      break;
    }
  }

  return {result: state_cnt_match};

  // throw new Error("NotImplemented");
}

function process_lisa(data) {
  const match = data.match(/\n(UNREALIZABLE|REALIZABLE)/);
  if (match) {
    return {
      result: capitalizedOnlyFirst(
        match[0].match(/UNREALIZABLE|REALIZABLE/)[0]
      ),
    };
  } else {
    return {
      result: "Stopped",
    };
  }
}

function process_nike(data) {
  const match = data.match(/(UNREALIZABLE|REALIZABLE)/);
  if (match) {
    return {
      result: capitalizedOnlyFirst(
        match[0].match(/UNREALIZABLE|REALIZABLE/)[0]
      ),
    };
  } else {
    return {
      result: "Stopped",
    };
  }
}

function process_lydia(data) {
  const match = data.match(
    /\[\d{4}\-\d{2}\-\d{2} \d{2}:\d{2}:\d{2}\.\d+\] \[lydia\] \[info\] \[main\] (unrealizable|realizable)\./
  );
  if (match) {
    return {
      result: capitalizedOnlyFirst(
        match[0].match(/unrealizable|realizable/)[0]
      ),
    };
  } else {
    return {
      result: "Stopped",
    };
  }
}

function process_RawSubAfSz(data) {
  const fourth_line_str = data.split('\n')[3];
  // console.log(fourth_line_str);
  const match = fourth_line_str.match(/and_af_size: (\d+)/);
  if (match)
    return {result: match[1]};
  else
    return {result: -1};
}


function process_SplitAndSubAfSz(data) {
  let match = null;
  const lines = data.split('\n');
  for (let i = 0; i < Math.min(lines.length, 10); i++)
  {
    if (match = lines[i].match(/and_af_size: (\d+)/))
      {
        break;
      }
  }
  if (match)
    {
      return {result: match[1]};
    }
  else
  {
    return {result: -1};
  }
}

const proces_funcs = {
  rawSubAfSz: {
    just_res: process_RawSubAfSz,
  },
  splitAndSubAfSz: {
    just_res: process_SplitAndSubAfSz,
  },
  ltlfsyn: {
    just_res: process_ltlfsyn,
  },
  ltlfsynSyft: {
    just_res: process_ltlfsynSyft,
  },
  ltlfsynSyft_Cases: {
    just_res: process_ltlfsynSyft_Cases,
  },
  ltlfsynSyft_Details: {
    just_res: process_ltlfsynSyft_Details,
  },
  lydia: {
    just_res: process_lydia,
  },
  lisa: {
    just_res: process_lisa,
  },
  nike: {
    just_res: process_nike,
  },
  lisaComp: {
    just_res: process_nike,
  },
  lydiaComp: {
    just_res: process_nike,
  },
};

function readLastNLines(filePath, n) {
  return new Promise((resolve, reject) => {
    fs.stat(filePath, (err, stats) => {
      if (err) {
        console.error("无法获取文件信息:", err);
        return;
      }

      const fileSize = stats.size;
      const chunkSize = 1024; // 每次读取的块大小
      let position = fileSize; // 初始位置为文件末尾
      let leftover = '';
      let lines = [];

      const readNextChunk = () => {
        const bytesToRead = Math.min(chunkSize, position); // 防止读取超出文件范围
        position -= bytesToRead;

        // 创建读取流，从当前 position 读取指定大小的字节
        const stream = fs.createReadStream(filePath, {
          start: position,
          end: position + bytesToRead - 1, // 从文件尾部倒着读取
          encoding: 'utf8'
        });

        stream.on('data', (chunk) => {
          // console.log(chunk);
          leftover = chunk + leftover; // 把新读取的块加在剩余的前面
          const splitLines = leftover.split('\n'); // 按行拆分

          leftover = splitLines.shift(); // 处理剩余的部分
          lines = splitLines.concat(lines); // 将新行合并到已有的行
          // console.log(lines.length);

          if (lines.length >= n) {
            lines = lines.slice(-n); // 只保留最后 n 行
            stream.destroy(); // 停止读取
            resolve({ data: lines.join('\n') });
          } else if (position > 0) {
            // console.log('position', position);
            readNextChunk(); // 继续读取上一块
          } else if (position <= 0) {
            stream.destroy();
            resolve({ data: [leftover, ...lines].join('\n') }); // 返回结果
          }
        });

        stream.on('error', (err) => {
          // console.error('读取文件出错:', err);
          reject(err);
        });
      };

      // 从末尾开始逐块读取
      readNextChunk();
    });
  })
}

async function isFileLargerThan100MB(filePath) {
  try {
      const stats = await fs.promises.stat(filePath);
      const fileSizeInBytes = stats.size;
      // console.log(fileSizeInBytes, filePath);
      const tenMB = 100 * 1024 * 1024; // 10MB 的字节数

      return fileSizeInBytes > tenMB;
  } catch (err) {
      console.error("无法获取文件信息:", err);
      throw err; // 可以抛出错误以便调用者处理
  }
}

async function get_res(filePath, processFunc) {
    // const too_large_flag = await isFileLargerThan100MB(filePath);
    // if (too_large_flag)
    // {
    //   // console.log(filePath, 'ERR_STRING_TOO_LONG');
    //   return { result: "FileLg100MB" }
    // }
  const { data } = await readLastNLines(filePath, 25).catch((err) => {
    console.log(filePath, err);
    return {data: "unknown error" }
  });
  if (data === null) {
    return {
      result: "NoResFile",
    };
  }
  if (data === "") {
    return {
      result: "EmptyResFile",
    };
  }
  if (data === null) {
    return {
      result: "Stopped",
    };
  }
  // console.log('beforeProcess');
  return processFunc(data);
}

module.exports = {
  readFileAsString,
  get_res,
  proces_funcs,
};
